(declare-fun v () Real)
(declare-fun d () Real)
(declare-fun b () Real)
(declare-fun m () Real)
(declare-fun t2uscore0dollarskuscore0 () Real)
(declare-fun z () Real)
(assert (not (exists ((ts2uscore0 Real)) (=> (or (and (and (= (<= ts2uscore0 ts2uscore0 t2uscore0dollarskuscore0) (>= v 0)) (>= t2uscore0dollarskuscore0 172)) (<= (- (div d d)) 0)) (<= z m)) (<= (/ 0 v) d)))))
(check-sat)
(declare-fun v () Real)
(declare-fun d () Real)
(declare-fun b () Real)
(declare-fun m () Real)
(declare-fun t2uscore0dollarskuscore0 () Real)
(declare-fun z () Real)
(assert (not (exists ((ts2uscore0 Real)) (=> (or (and (and (= (<= ts2uscore0 ts2uscore0 t2uscore0dollarskuscore0) (>= v 0)) (>= t2uscore0dollarskuscore0 172)) (<= (- (div d d)) 0)) (<= z m)) (<= (/ 0 v) d)))))
(check-sat)
